P:({k}). (i:. (j:i. P(j))  P(i))  (i:. P(i)) 

latex

ProofTree

Definitions	x(s), P  Q, , , x:A. B(x), t  T, Y, False, A, A  B, i  j , suptype(S; T), S  T, {i..j}, P  Q, i  j < k, P  Q, Dec(P)
Lemmas	le wf, int seg wf, nat wf, ge wf, nat properties, decidable int equal